package tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class ChooseRuleBranchingPoint extends BranchingPoint {
	private int index;

	private ObjectRoleAssertion roleAssertion;

	private Set<WorldConstraintSystem> dependencySet = new HashSet<WorldConstraintSystem>();

	private Formula branchCause;

	private List<WorldElement> formulas = new ArrayList<WorldElement>();

	public Formula getBranchCause() {
		return branchCause;
	}

	public void setBranchCause(Formula branchCause) {
		this.branchCause = branchCause;
	}

	public boolean addFormula(WorldElement o) {
		return formulas.add(o);
	}

	protected List<WorldElement> getFormulas() {
		return formulas;
	}

	private Set<WorldConstraintSystem> getDependencySet() {
		return dependencySet;
	}

	public ObjectRoleAssertion getRoleAssertion() {
		return roleAssertion;
	}

	public void setRoleAssertion(ObjectRoleAssertion roleAssertion) {
		this.roleAssertion = roleAssertion;
	}

	@Override
	public boolean hasNext() {
		return index < getFormulas().size();
	}

	public WorldConstraintSystem next() throws UnsatisfiableException {
		WorldConstraintSystem result = null;
		if (index == 0) {
			ConceptAssertion ca = (ConceptAssertion) getFormulas().get(index++);
			result = getWcs().copy();
			result.setId(getWcs().getId() + 1);
			ABox abox = result.getWorld(getWorld().getName()).getABox();
			result.getData().getDependencyManager()
					.move(ca, getRoleAssertion());
			result.getData().getDependencyManager().add(ca, getWcs());
			abox.add(ca);
		} else if (index == 1) {
			getDependencySet().addAll(getLastBranchDependencies());
			getDependencySet().remove(getWcs());
			result = getWcs();
			ABox abox = result.getWorld(getWorld().getName()).getABox();
			ConceptAssertion ca = (ConceptAssertion) getFormulas().get(index++);
			result.getData().getDependencyManager().addAll(ca,
					getDependencySet());
			result.getData().getDependencyManager().move(ca, getBranchCause());
			result.getData().getDependencyManager()
					.move(ca, getRoleAssertion());
			abox.add(ca);
		}
		return result;
	}

}
